(declare-fun GUqRZLZ_new () String)
(declare-fun shifted1_s () String)
(assert (= (str.at shifted1_s 2) (str.at (str.substr GUqRZLZ_new 0 (str.len shifted1_s)) 3)))
(assert (not (= (str.at (str.substr GUqRZLZ_new 0 (str.len shifted1_s)) 3) (str.at (str.substr GUqRZLZ_new 0 (str.len shifted1_s)) 6))))
(assert (not (= (str.at shifted1_s 3) (str.at shifted1_s 5))))
(assert (not (= (str.at shifted1_s 3) (str.at (str.substr GUqRZLZ_new 0 (str.len shifted1_s)) 4))))
(assert (not (= (str.at (str.substr GUqRZLZ_new 0 (str.len shifted1_s)) 4) (str.at (str.substr GUqRZLZ_new 0 (str.len shifted1_s)) 6))))
(assert (not (= (str.at shifted1_s 4) (str.at shifted1_s 5))))
(assert (= (str.len (str.substr GUqRZLZ_new 0 (str.len shifted1_s))) 7))
(assert (= (str.at (str.substr GUqRZLZ_new 0 (str.len shifted1_s)) 5) (str.at shifted1_s 6)))
(assert (= (str.len shifted1_s) 7))
(assert (distinct (str.replace (str.replace GUqRZLZ_new shifted1_s (str.at GUqRZLZ_new (str.len GUqRZLZ_new))) "AZHxb" (str.at GUqRZLZ_new (str.len GUqRZLZ_new))) ""))
(check-sat)
